(** Based on "Elements of Set Theory" Chapter 5 Part 6 **)
(** Coq coding by choukh, July 2020 **)

Require Export ZFC.EST5_5.

(*** EST第五章6：实数绝对值，非负实数乘法，正实数乘法逆元 ***)

(** 实数绝对值 **)
Definition RealAbs : set → set := λ x, x ∪ -x.
Notation "| r |" := (RealAbs r) : Real_scope.

Lemma realAbs_nonNeg_id : ∀ x, realNonNeg x → |x| = x.
Proof with neauto.
  intros x [Hpos|H0].
  - assert (Hx: x ∈ ℝ) by (apply binRelE2 in Hpos as [_ []]; auto).
    apply realPos_rat0 in Hpos as H0...
    apply ExtAx. intros q. split; intros Hq; revgoals.
    apply BUnionI1... apply BUnionE in Hq as []...
    apply SepE in H as [Hq [s [Hs [Hlt H]]]].
    eapply realE2_1 in H; revgoals... apply ratAddInv_ran...
    apply ratPos_neg in H. rewrite ratAddInv_double in H...
    assert (Hnq: ratNeg q) by (eapply ratLt_tranr; eauto).
    eapply realE2; revgoals...
  - subst. apply ExtAx. intros q. split; intros Hq.
    + apply BUnionE in Hq as []... rewrite realAddInv_0 in H...
    + apply BUnionI1...
Qed.

Lemma realAbs_unsigned_nonNeg : ∀x ∈ ℝ, |x| = x → realNonNeg x.
Proof with neauto.
  intros x Hx Heq. apply realLeq... intros q Hq.
  apply SepE in Hq as [Hq Hlt]. rewrite <- Heq.
  destruct (classic (Rat 0 ∈ x)).
  - apply BUnionI1. eapply realE2; revgoals...
  - apply BUnionI2. apply SepI... exists (Rat 0).
    split... split... rewrite ratAddInv_0...
Qed.

Lemma realAbs_nonPos_flip : ∀ x, realNonPos x → |x| = -x.
Proof with neauto.
  intros x [Hneg|Heq].
  - assert (Hx: x ∈ ℝ) by (apply binRelE2 in Hneg as []; auto).
    apply realNeg_pos in Hneg as Hpos.
    apply realPos_rat0 in Hpos as H0; [|apply realAddInv_ran; auto].
    apply ExtAx. intros q. split; intros Hq; revgoals.
    apply BUnionI2... apply BUnionE in Hq as [Hqx|]...
    assert (Hq: q ∈ ℚ) by (apply (real_sub_rat x Hx); auto).
    apply SepI... apply SepE in H0 as [_ [s [Hs [Hlt Hout]]]].
    exists s. split... split... eapply ratLt_tranr...
    eapply realE2_1... intros H. apply realPos_rat0 in H...
    eapply realLt_irrefl. eapply realLt_tranr...
  - subst. apply ExtAx. intros q. split; intros Hq.
    + apply BUnionE in Hq as []... rewrite realAddInv_0...
    + apply BUnionI2...
Qed.

Lemma realAbs_flip_nonPos : ∀x ∈ ℝ, |x| = -x → realNonPos x.
Proof with neauto.
  intros x Hx Heq. apply realLeq_addInv'...
  rewrite realAddInv_0. apply realLeq... apply realAddInv_ran...
  intros q Hq. apply SepE in Hq as [Hq Hlt]. rewrite <- Heq.
  destruct (classic (Rat 0 ∈ x)).
  - apply BUnionI1. eapply realE2; revgoals...
  - apply BUnionI2. apply SepI... exists (Rat 0).
    split... split... rewrite ratAddInv_0...
Qed.

Lemma realAbs_eq_0 : ∀x ∈ ℝ, |x| = Real 0 → x = Real 0.
Proof with nauto.
  intros x Hx H0. destruct (classic (realNonNeg x))...
  rewrite (realAbs_nonNeg_id _ H) in H0...
  apply realNeg_not_nonNeg in H...
  apply realNeg_nonPos in H...
  rewrite (realAbs_nonPos_flip _ H) in H0.
  assert (--x = -Real 0) by congruence.
  rewrite realAddInv_double, realAddInv_0 in H1...
Qed.

Lemma realAbs_unsigned : ∀x ∈ ℝ, | -x | = |x|.
Proof with auto.
  intros x Hx.
  assert (Hx': -x ∈ ℝ) by (apply realAddInv_ran; auto).
  destruct (classic (realNonNeg (-x))).
  - rewrite (realAbs_nonNeg_id _ H).
    apply realNonNeg_nonPos in H...
    rewrite realAddInv_double in H...
    rewrite (realAbs_nonPos_flip _ H)...
  - apply realNeg_not_nonNeg in H...
    apply realNeg_nonPos in H...
    rewrite (realAbs_nonPos_flip _ H), realAddInv_double...
    apply realNonPos_nonNeg in H... rewrite realAddInv_double in H...
    rewrite (realAbs_nonNeg_id _ H)...
Qed.

Lemma realAbs_ran : ∀x ∈ ℝ, |x| ∈ ℝ.
Proof with auto.
  intros x Hx. destruct (classic (realNonNeg x)).
  - apply realAbs_nonNeg_id in H. rewrite H...
  - apply realNeg_not_nonNeg in H...
    apply realNeg_nonPos in H...
    apply realAbs_nonPos_flip in H. rewrite H...
    apply realAddInv_ran...
Qed.

Theorem realAbs_nonNeg : ∀x ∈ ℝ, realNonNeg (|x|).
Proof with neauto.
  intros x Hx. destruct (classic (realNonNeg x)).
  - rewrite (realAbs_nonNeg_id _ H)...
  - apply realNeg_not_nonNeg in H...
    apply realNeg_nonPos in H...
    apply realAbs_nonPos_flip in H as Heq. rewrite Heq.
    apply realNonPos_nonNeg...
Qed.

Lemma realPos_ratPos : ∀x ∈ ℝ,
  realPos x → ∃q ∈ ℚ, q ∈ x ∧ ratPos q.
Proof with auto.
  intros x Hx Hpx. apply realE3... apply realPos_rat0...
Qed.

Lemma realPos_ratNonNeg : ∀x ∈ ℝ,
  realPos x → ∃q ∈ x, ratNonNeg q.
Proof with auto.
  intros x Hx Hpx. exists (Rat 0). split...
  apply realPos_rat0... right...
Qed.

Lemma realNonPos_ratNeg : ∀x ∈ ℝ,
  realNonPos x → ∃q ∈ x, ratNeg q.
Proof with nauto.
  intros x Hx Hnpx. apply realLeq in Hnpx...
  apply realE0 in Hx as [r [Hrq Hrx]].
  exists r. split... apply Hnpx in Hrx.
  apply SepE in Hrx as [_ Hnr]...
Qed.

Lemma realNonPos_ratNonPos : ∀x ∈ ℝ,
  realNonPos x → ∃q ∈ x, ratNonPos q.
Proof with nauto.
  intros x Hx Hnpx.
  apply realNonPos_ratNeg in Hnpx as [q [Hqx Hnq]]...
  exists q. split... left...
Qed.

Lemma realE1'_ratPos : ∀x ∈ ℝ, realNonNeg x →
  ∃r ∈ ℚ, (∀q ∈ x, q <𝐪 r) ∧ ratPos r.
Proof with neauto.
  intros x Hx Hnnx. assert (Hx' := Hx).
  apply realE1 in Hx' as [r [Hrq Hrx]].
  exists (r + Rat 1)%q. split... apply ratAdd_ran... split.
  intros q Hq. apply (real_sub_rat _ Hx) in Hq as Hqq.
  assert (Hlt: r <𝐪 (r + Rat 1)%q). {
    rewrite <- (ratAdd_ident r) at 1...
    apply ratAdd_preserve_lt'... apply ratPos_sn.
  }
  eapply ratLt_tranr; revgoals. apply Hlt. eapply realE2_1...
  cut (ratNonNeg r). intros [Hpr|H0].
  unfold ratPos. rewrite <- (ratAdd_ident (Rat 0))...
  apply ratAdd_preserve_lt_tran... apply ratPos_sn.
  subst. rewrite ratAdd_ident'... destruct Hnnx. 
  - left. apply realPos_rat0 in H... eapply realE2_1...
  - subst. destruct (classic (r = Rat 0))... right...
    apply ratLt_connected in H as []...
    exfalso. apply Hrx. apply SepI... left...
Qed.

(** 非负实数乘法 **)
Definition RealNonNegMul : set → set → set := λ x y,
  let P := {p ∊ x × y | λ p, ratNonNeg (π1 p) ∧ ratNonNeg (π2 p)} in
  Real 0 ∪ {λ p, (π1 p ⋅ π2 p)%q | p ∊ P}.
Notation "x ⋅₊ y" := (RealNonNegMul x y) (at level 45) : Real_scope.

Lemma realNonNegMulI0 : ∀ x y ∈ ℝ, ∀ s, ratNeg s → s ∈ x ⋅₊ y.
Proof with auto.
  intros x Hx y Hy s Hps. apply BUnionI1.
  apply SepI... apply ratNeg_rat...
Qed.

Lemma realNonNegMulI1 : ∀ x y ∈ ℝ, ∀q ∈ x, ∀r ∈ y,
  ratNonNeg q → ratNonNeg r → (q ⋅ r)%q ∈ x ⋅₊ y.
Proof with auto.
  intros x Hx y Hy q Hqx r Hry Hnnq Hnnr.
  apply BUnionI2. apply ReplAx.
  exists <q, r>. split; zfc_simple. apply SepI.
  apply CProdI... zfc_simple. split...
Qed.

Lemma realNonNegMulE : ∀ x y ∈ ℝ, ∀s ∈ x ⋅₊ y, s ∈ Real 0 ∨
  ∃q ∈ ℚ, ∃r ∈ ℚ, (q ∈ x ∧ r ∈ y) ∧
    (ratNonNeg q ∧ ratNonNeg r) ∧ s = (q ⋅ r)%q.
Proof with auto.
  intros x Hx y Hy s Hs.
  apply BUnionE in Hs as []... right.
  apply ReplAx in H as [p [Hp Hs]].
  apply SepE in Hp as [Hp [H1 H2]].
  apply CProdE1 in Hp as [q [Hq [r [Hr Hp]]]].
  subst. zfc_simple.
  exists q. split... apply (real_sub_rat _ Hx)...
  exists r. split... apply (real_sub_rat _ Hy)...
Qed.

Lemma realNonNegMul_sub_rat : ∀ x y ∈ ℝ, x ⋅₊ y ∈ 𝒫 ℚ.
Proof with auto.
  intros x Hx y Hy. apply PowerAx. intros s Hs.
  apply realNonNegMulE in Hs as []... apply SepE1 in H...
  destruct H as [q [Hq [r [Hr [_ [_ Heq]]]]]].
  subst. apply ratMul_ran...
Qed.

Close Scope Real_scope.
Open Scope Rat_scope.

Lemma realNonNegMul_ran : ∀ x y ∈ ℝ,
  realNonNeg x → realNonNeg y → (x ⋅₊ y)%r ∈ ℝ.
Proof with neauto.
  intros x Hxr y Hyr Hnnx Hnny.
  apply SepI. apply realNonNegMul_sub_rat... repeat split.
  - apply EmptyNI. destruct (classic (x = Real 0 ∨ y = Real 0)).
    + destruct H.
      * assert (Hnpx: realNonPos x) by (right; auto).
        apply realNonPos_ratNeg in Hnpx as [q [Hqy Hnq]]...
        exists q. apply realNonNegMulI0...
      * assert (Hnpy: realNonPos y) by (right; auto).
        apply realNonPos_ratNeg in Hnpy as [r [Hrx Hnr]]...
        exists r. apply realNonNegMulI0...
    + apply not_or_and in H as [Hx0 Hy0].
      destruct Hnnx; destruct Hnny; [clear Hx0 Hy0|exfalso; auto..].
      apply realPos_ratNonNeg in H as [q [Hq Hnnq]]...
      apply realPos_ratNonNeg in H0 as [r [Hr Hnnr]]...
      exists (q ⋅ r). apply realNonNegMulI1...  
  - assert (Hx' := Hxr). assert (Hy' := Hyr).
    apply realE1'_ratPos in Hx' as [q [Hq [H1 Hpq]]]...
    apply realE1'_ratPos in Hy' as [r [Hr [H2 Hpr]]]...
    assert (Hqr : q ⋅ r ∈ ℚ) by (apply ratMul_ran; auto).
    apply ExtNI. exists (q ⋅ r). split... intros H.
    apply (ratLt_irrefl (q ⋅ r))...
    cut (∀p ∈ (x ⋅₊ y)%r, p <𝐪 q ⋅ r). intros Hlt. apply Hlt...
    intros p Hp. apply realNonNegMulE in Hp as []...
    + apply SepE in H0 as [_ H0].
      eapply ratLt_tranr. apply H0.
      apply ratMul_pos_prod...
    + destruct H0 as [s [Hsq [t [Htq [[Hs Ht] [[Hnns Hnnt] Heq]]]]]].
      subst. apply H1 in Hs. apply H2 in Ht.
      destruct Hnnt as [Hpt|H0].
      eapply ratMul_preserve_lt_tran...
      subst. rewrite ratMul_0_r... apply ratMul_pos_prod...
  - intros p Hp q Hq Hqxy Hlt.
    apply realNonNegMulE in Hqxy as []; auto; [|
      destruct (classic (ratNeg p)) as [|Hnnp]]; auto; [| |
        destruct H as [s [Hsq [t [Htq [[Hs Ht]
          [[[Hps|H0] Hnnt] Heq]]]]]]; revgoals]; subst.
    + apply realNonNegMulI0...
      apply SepE in H as [_ H0]. eapply ratLt_tranr...
    + apply realNonNegMulI0...
    + apply realNonNegMulI0...
      rewrite ratMul_0_l in Hlt...
    + assert (Hsq': s ∈ ℚ'). {
        apply nzRatI0... apply rat_neq_0...
      }
      assert (Hrsq: s⁻¹ ∈ ℚ). {
        apply nzRatE1. apply ratMulInv_ran...
      }
      assert (Hprs: ratPos s⁻¹) by (apply ratPos_mulInv; auto).
      assert (Heq: p = s ⋅ (p / s)). {
        rewrite (ratMul_comm p), <- ratMul_assoc,
        ratMulInv_annih, ratMul_ident'...
      }
      assert (Hlt': p / s <𝐪 t). {
        rewrite <- (ratMul_ident t), <- (ratMulInv_annih s),
          <- ratMul_assoc... apply ratMul_preserve_lt...
        apply ratMul_ran... rewrite ratMul_comm...
      }
      rewrite Heq. apply realNonNegMulI1...
      eapply realE2; revgoals... apply ratMul_ran... left...
      apply ratNonNeg_not_neg in Hnnp as []...
      left. apply ratMul_pos_prod...
      right. subst. rewrite ratMul_0_l...
  - intros p Hp. apply realNonNegMulE in Hp as []...
    + apply SepE in H as [Hpq Hp0]. 
      assert (Hpd2q: p / Rat 2 ∈ ℚ) by (apply ratMul_ran; nauto).
      assert (Hnpq: - p ∈ ℚ) by (apply ratAddInv_ran; auto).
      exists (p / Rat 2). split.
      * apply realNonNegMulI0... unfold ratNeg.
        rewrite <- (ratMul_ident (Rat 0)),
          <- (ratMulInv_annih (Rat 2)), <- ratMul_assoc, ratMul_0_l...
        apply ratMul_preserve_lt...
      * apply ratLt_addInv... rewrite <- (ratMul_ident (-p)),
          <- ratMul_addInv_l, ratMul_comm, (ratMul_comm (-p))...
        apply ratMul_preserve_lt...
        apply ratNeg_pos... apply ratLt_r2_1.
    + destruct H as [s [Hsq [t [Htq [[Hs Ht] [[Hnns Hnnt] Heq]]]]]].
      apply realE3 in Hs as [q [Hqq [Hqx H1]]]...
      apply realE3 in Ht as [r [Hrq [Hry H2]]]...
      assert (Hpq: ratPos q). {
        destruct Hnns. eapply ratLt_tranr... subst...
      }
      assert (Hpr: ratPos r). {
        destruct Hnnt. eapply ratLt_tranr.
        apply H. apply H2. subst...
      }
      exists (q ⋅ r). split. apply realNonNegMulI1...
      left... left... destruct Hnnt; revgoals; subst.
      * rewrite ratMul_0_r... apply ratMul_pos_prod...
      * apply ratMul_preserve_lt_tran...
Qed.

Close Scope Rat_scope.
Open Scope Real_scope.

Lemma realNonNegMul_comm : ∀ x y ∈ ℝ,
  realNonNeg x → realNonNeg y → x ⋅₊ y = y ⋅₊ x.
Proof with auto.
  intros x Hx y Hy Hnnx Hnny.
  apply ExtAx. intros p. split; intros Hp.
  - assert (Hpq: p ∈ ℚ). {
      apply real_sub_rat in Hp... apply realNonNegMul_ran...
    }
    apply realNonNegMulE in Hp as []; auto; [|
      destruct (classic (ratNeg p)) as [|Hnnp]]...
    + apply BUnionI1...
    + apply realNonNegMulI0...
    + destruct H as [s [Hsq [t [Htq [[Hs Ht] [[Hnns Hnnt] Heq]]]]]].
      rewrite Heq, ratMul_comm... apply realNonNegMulI1...
  - assert (Hpq: p ∈ ℚ). {
      apply real_sub_rat in Hp... apply realNonNegMul_ran...
    }
    apply realNonNegMulE in Hp as []; auto; [|
      destruct (classic (ratNeg p)) as [|Hnnp]]...
    + apply BUnionI1...
    + apply realNonNegMulI0...
    + destruct H as [s [Hsq [t [Htq [[Hs Ht] [[Hnns Hnnt] Heq]]]]]].
      rewrite Heq, ratMul_comm... apply realNonNegMulI1...
Qed.

Lemma realNonNegMul_0_r : ∀x ∈ ℝ, x ⋅₊ Real 0 = Real 0.
Proof with nauto.
  intros x Hx. apply ExtAx. intros p. split; intros Hp.
  - apply realNonNegMulE in Hp as []... exfalso.
    destruct H as [_ [_ [t [_ [[_ Ht] [[_ Hnnt] _]]]]]].
    apply SepE in Ht as [Htq Hnt].
    apply ratNonNeg_not_neg in Hnnt...
  - apply BUnionI1...
Qed.

Lemma realNonNegMul_0_l : ∀x ∈ ℝ, Real 0 ⋅₊ x = Real 0.
Proof with nauto.
  intros x Hx. apply ExtAx. intros p. split; intros Hp.
  - apply realNonNegMulE in Hp as []... exfalso.
    destruct H as [q [_ [_ [_ [[Hq _] [[Hnnq _] _]]]]]].
    apply SepE in Hq as [Hqq Hnq].
    apply ratNonNeg_not_neg in Hnnq...
  - apply BUnionI1...
Qed.

Lemma realNonNegMul_preserve_leq : ∀ x y z ∈ ℝ,
  realNonNeg x → realNonNeg y → realPos z → 
  x ≤ y → x ⋅₊ z ≤ y ⋅₊ z.
Proof with eauto.
  intros x Hx y Hy z Hz Hnnx Hnny Hpz Hleq.
  apply realPos_nonNeg in Hpz as Hnnz...
  apply realLeqE in Hleq. apply realLeqI.
  apply realNonNegMul_ran... apply realNonNegMul_ran...
  intros p Hp. apply realNonNegMulE in Hp as []...
  - apply BUnionI1...
  - destruct H as [q [_ [r [_ [[Hq Hr] [[Hnnq Hnnr] Heq]]]]]].
    destruct Hnny as [Hpy|Hy0].
    + rewrite Heq. apply realNonNegMulI1... apply Hleq...
    + exfalso. subst. apply Hleq in Hq.
      apply SepE in Hq as [Hq Hq0].
      apply ratNonNeg_not_neg in Hnnq...
Qed.

Lemma realNonNegMul_nonNeg_prod : ∀ x y ∈ ℝ,
  realNonNeg x → realNonNeg y → realNonNeg (x ⋅₊ y).
Proof with nauto.
  intros x Hxr y Hyr Hnnx Hnny.
  destruct Hnny as [Hpy|Hy0].
  - unfold realNonNeg. rewrite <- (realNonNegMul_0_l y)...
    apply realNonNegMul_preserve_leq... right...
  - subst. rewrite realNonNegMul_0_r... right...
Qed.

Lemma realNonNegMul_pos_prod : ∀ x y ∈ ℝ,
  realPos x → realPos y → realPos (x ⋅₊ y).
Proof with nauto.
  intros x Hxr y Hyr Hpx Hpy. apply realPos_rat0.
  apply realNonNegMul_ran; auto; apply realPos_nonNeg...
  rewrite <- (ratMul_0_l (Rat 0))... apply realNonNegMulI1...
  apply realPos_rat0... apply realPos_rat0... right... right...
Qed.

Lemma realNonNegMul_assoc : ∀ x y z ∈ ℝ,
  realNonNeg x → realNonNeg y → realNonNeg z →
  (x ⋅₊ y) ⋅₊ z = x ⋅₊ (y ⋅₊ z).
Proof with auto.
  intros x Hx y Hy z Hz Hnnx Hnny Hnnz.
  assert (Hxyr: x ⋅₊ y ∈ ℝ) by (apply realNonNegMul_ran; auto).
  assert (Hyzr: y ⋅₊ z ∈ ℝ) by (apply realNonNegMul_ran; auto).
  apply ExtAx. intros p. split; intros Hp.
  - assert (Hpq: p ∈ ℚ). {
      apply real_sub_rat in Hp... apply realNonNegMul_ran...
      apply realNonNegMul_nonNeg_prod...
    }
    apply realNonNegMulE in Hp as []... apply BUnionI1...
    destruct H as [q [_ [t [Htq [[Hq Ht] [[Hnnq Hnnt] Hpeq]]]]]].
    apply realNonNegMulE in Hq as []...
    + exfalso. apply SepE in H as [Hqq Hnq].
      apply ratNonNeg_not_neg in Hnnq...
    + destruct H as [r [Hrq [s [Hsq [[Hr Hs] [[Hnnr Hnns] Hqeq]]]]]].
      assert (Hnnst: ratNonNeg (s ⋅ t)%q)
        by (apply ratMul_nonNeg_prod; auto).
      subst. rewrite ratMul_assoc...
      apply realNonNegMulI1... apply realNonNegMulI1...
  - assert (Hpq: p ∈ ℚ). {
      apply real_sub_rat in Hp... apply realNonNegMul_ran...
      apply realNonNegMul_nonNeg_prod...
    }
    apply realNonNegMulE in Hp as []... apply BUnionI1...
    destruct H as [q [Hqq [t [_ [[Hq Ht] [[Hnnq Hnnt] Hpeq]]]]]].
    apply realNonNegMulE in Ht as []...
    + exfalso. apply SepE in H as [Htq Hnt].
      apply ratNonNeg_not_neg in Hnnt...
    + destruct H as [r [Hrq [s [Hsq [[Hr Hs] [[Hnnr Hnns] Hteq]]]]]].
      assert (Hnnqr: ratNonNeg (q ⋅ r)%q)
        by (apply ratMul_nonNeg_prod; auto).
      subst. rewrite <- ratMul_assoc...
      apply realNonNegMulI1... apply realNonNegMulI1...
Qed.

Lemma realAddE_nonNeg : ∀ x y ∈ ℝ, ∀q ∈ ℚ,
  realPos x → realPos y → ratNonNeg q → q ∈ x + y →
  ∃ r s ∈ ℚ, (r ∈ x ∧ s ∈ y) ∧
    (ratNonNeg r ∧ ratNonNeg s) ∧ (r + s)%q = q.
Proof with neauto.
  intros x Hx y Hy q Hqq Hpx Hpy Hnnq Hq.
  apply ReplAx in Hq as [t [Ht Heq]]. apply CProdE1 in Ht
    as [r [Hr [s [Hs Ht]]]]. subst. zfc_simple.
  assert (Hrq: r ∈ ℚ) by (eapply real_sub_rat; revgoals; eauto).
  assert (Hsq: s ∈ ℚ) by (eapply real_sub_rat; revgoals; eauto).
  destruct (classic (ratNeg r)); destruct (classic (ratNeg s)).
  - exfalso. apply ratNonNeg_not_neg in Hnnq...
    apply Hnnq. apply ratAdd_neg_sum...
  - exists (Rat 0). split... exists (r + s)%q. repeat split...
    + apply realPos_rat0...
    + cut ((r + s)%q <𝐪 s). intros Hlt. eapply realE2; revgoals...
      rewrite <- (ratAdd_ident' s) at 2... apply ratAdd_preserve_lt...
    + right... + rewrite ratAdd_ident'...
  - exists (r + s)%q. split... exists (Rat 0). repeat split...
    + cut ((r + s)%q <𝐪 r). intros Hlt. eapply realE2; revgoals...
      rewrite <- (ratAdd_ident r) at 2... apply ratAdd_preserve_lt'...
    + apply realPos_rat0...
    + right... + rewrite ratAdd_ident...
  - apply ratNonNeg_not_neg in H... apply ratNonNeg_not_neg in H0...
    exists r. split... exists s. split...
Qed.

Lemma realNonNegMul_distr : ∀ x y z ∈ ℝ,
  realNonNeg x → realNonNeg y → realNonNeg z →
  x ⋅₊ (y + z) = x ⋅₊ y + x ⋅₊ z.
Proof with nauto.
  intros x Hx y Hy z Hz Hnnx Hnny Hnnz.
  assert (Hxyr: x ⋅₊ y ∈ ℝ) by (apply realNonNegMul_ran; auto).
  assert (Hxzr: x ⋅₊ z ∈ ℝ) by (apply realNonNegMul_ran; auto).
  assert (Hsumr: y + z ∈ ℝ) by (apply realAdd_ran; auto).
  apply ExtAx. intros p. split; intros Hp.
  - apply realNonNegMulE in Hp as []...
    + cut (Real 0 ⊆ x ⋅₊ y + x ⋅₊ z). intros Hsub. apply Hsub...
      apply realLeq... apply realAdd_ran...
      apply realAdd_nonNeg_sum; auto;
      apply realNonNegMul_nonNeg_prod...
    + destruct H as [q [Hqq [t [Htq [[Hq Ht] [[Hnnq Hnnt] Hpeq]]]]]].
      destruct Hnny; destruct Hnnz; subst.
      * apply realAddE_nonNeg in Ht
          as [r [Hrq [s [Hsq [[Hr Hs] [[Hnnr Hnns] Heq]]]]]]...
        subst. rewrite ratMul_distr... apply realAddI2...
        apply realNonNegMulI1... apply realNonNegMulI1...
      * rewrite realAdd_ident in Ht...
        rewrite realNonNegMul_0_r, realAdd_ident...
        apply realNonNegMulI1...
      * rewrite realAdd_ident' in Ht...
        rewrite realNonNegMul_0_r, realAdd_ident'...
        apply realNonNegMulI1...
      * exfalso. apply ratNonNeg_not_neg in Hnnt... apply Hnnt.
        rewrite realAdd_ident in Ht... apply SepE2 in Ht...
  - destruct Hnnx as [Hpx|]; revgoals; [|
      destruct (classic (y = Real 0 ∨ z = Real 0)); [
        destruct H |
        apply not_or_and in H as [Hy0 Hz0];
        destruct Hnny as [Hpy|]; destruct Hnnz as [Hpz|];
          [clear Hy0 Hz0|exfalso; auto..]
    ]]; subst.
    + rewrite realNonNegMul_0_l... rewrite realNonNegMul_0_l,
        realNonNegMul_0_l, realAdd_ident in Hp...
    + rewrite realAdd_ident'...
      rewrite realNonNegMul_0_r, realAdd_ident' in Hp...
    + rewrite realAdd_ident...
      rewrite realNonNegMul_0_r, realAdd_ident in Hp...
    + assert (Hpq: p ∈ ℚ). {
        apply real_sub_rat in Hp... apply realAdd_ran...
      }
      destruct (classic (ratNeg p)) as [|Hnnp]. apply realNonNegMulI0...
      apply ratNonNeg_not_neg in Hnnp...
      apply realAddE_nonNeg in Hp
        as [q [Hqq [r [Hrq [[Hq Hr] [_ Heq]]]]]];
        auto; [|apply realNonNegMul_pos_prod; auto..].
      Close Scope Real_scope.
      Open Scope Rat_scope.
      apply realNonNegMulE in Hq as [Hq|Hq];
      apply realNonNegMulE in Hr as [Hr|Hr]...
      * exfalso. subst. apply ratNonNeg_not_neg in Hnnp...
        apply Hnnp. apply ratAdd_neg_sum...
        apply SepE2 in Hq... apply SepE2 in Hr...
      * destruct Hr as [s [Hsq [t [Htq [[Hs Ht] [[Hnns Hnnt] Hreq]]]]]].
        destruct Hnns; revgoals; subst.
        rewrite ratMul_0_l, ratAdd_ident... apply BUnionI1...
        assert (Hs': s ∈ ℚ'). {
          apply nzRatI0... apply rat_neq_0...
        }
        assert (Hrsq: s⁻¹ ∈ ℚ). {
          apply nzRatE1. apply ratMulInv_ran...
        }
        assert (Hqsq: q/s ∈ ℚ) by (apply ratMul_ran; auto).
        assert (Hqs0: q/s <𝐪 Rat 0). {
          rewrite ratMul_comm... apply ratMul_neg_prod...
          apply ratPos_mulInv... apply SepE2 in Hq...
        }
        assert (Hnnsum: ratNonNeg (q/s + t)). {
          unfold ratNonNeg. rewrite <- (ratMul_ident t),
            <- (ratMulInv_annih s), <- ratMul_assoc, (ratMul_comm t),
            <- ratMul_distr', <- (ratMul_0_l s⁻¹); [|auto..].
          apply ratMul_preserve_leq... apply ratPos_mulInv...
        }
        replace (q + s ⋅ t) with (s ⋅ (q/s + t)).
        apply realNonNegMulI1... apply realAddI2...
        eapply realE2; revgoals; [eauto|nauto..]. apply realPos_rat0... left...
        rewrite ratMul_distr, (ratMul_comm q), <- ratMul_assoc,
          ratMulInv_annih, ratMul_ident'; [|auto..]...
      * destruct Hq as [s [Hsq [t [Htq [[Hs Ht] [[Hnns Hnnt] Hqeq]]]]]].
        destruct Hnns; revgoals; subst.
        rewrite ratMul_0_l, ratAdd_ident'... apply BUnionI1...
        assert (Hs': s ∈ ℚ'). {
          apply nzRatI0... apply rat_neq_0...
        }
        assert (Hrsq: s⁻¹ ∈ ℚ). {
          apply nzRatE1. apply ratMulInv_ran...
        }
        assert (Hrdsq: r/s ∈ ℚ) by (apply ratMul_ran; auto).
        assert (Hrs0: r/s <𝐪 Rat 0). {
          rewrite ratMul_comm... apply ratMul_neg_prod...
          apply ratPos_mulInv... apply SepE2 in Hr...
        }
        assert (Hnnsum: ratNonNeg (t + r/s)). {
          unfold ratNonNeg. rewrite <- (ratMul_ident t),
            <- (ratMulInv_annih s), <- ratMul_assoc, (ratMul_comm t),
            <- ratMul_distr', <- (ratMul_0_l s⁻¹); [|auto..].
          apply ratMul_preserve_leq; nauto. apply ratPos_mulInv... 
        }
        replace (s ⋅ t + r) with (s ⋅ (t + r/s)).
        apply realNonNegMulI1... apply realAddI2...
        eapply realE2; revgoals; [eauto|nauto..].
        apply realPos_rat0... left...
        rewrite ratMul_distr, (ratMul_comm r), <- ratMul_assoc,
          ratMulInv_annih, ratMul_ident'; [|auto..]...
      * destruct Hq as [s [Hsq [t [Htq [[Hs Ht] [[Hnns Hnnt] Hqeq]]]]]].
        destruct Hr as [u [Huq [v [Hvq [[Hu Hv] [[Hnnu Hnnv] Hreq]]]]]].
        destruct Hnns as [Hps|]; revgoals; subst. {
          rewrite ratMul_0_l, ratAdd_ident'; [|auto..].
          apply realNonNegMulI1... rewrite <- ratAdd_ident'...
          apply realAddI2... apply realPos_rat0...
        }
        destruct Hnnt as [Hpt|]; revgoals; subst. {
          rewrite ratMul_0_r, ratAdd_ident'; [|auto..].
          apply realNonNegMulI1... rewrite <- ratAdd_ident'...
          apply realAddI2...
        }
        destruct Hnnu as [Hpu|]; revgoals; subst. {
          rewrite ratMul_0_l, ratAdd_ident; [|auto..].
          apply realNonNegMulI1... rewrite <- ratAdd_ident...
          apply realAddI2... apply realPos_rat0... left... left...
        }
        destruct Hnnv as [Hpv|]; revgoals; subst. {
          rewrite ratMul_0_r, ratAdd_ident; [|auto..].
          apply realNonNegMulI1... rewrite <- ratAdd_ident...
          apply realAddI2... left... left...
        }
        destruct (classic (s = u)). {
          subst. rewrite <- ratMul_distr...
          apply realNonNegMulI1... apply realAddI2... left...
          apply ratAdd_nonNeg_sum... left... left...
        }
        apply ratLt_connected in H as [Hsu|Hus]... {
          assert (Hu': u ∈ ℚ'). {
            apply nzRatI0... apply rat_neq_0...
          }
          assert (Hruq: u⁻¹ ∈ ℚ). {
            apply nzRatE1. apply ratMulInv_ran...
          }
          assert (Hpru: ratPos u⁻¹) by (apply ratPos_mulInv; auto).
          assert (Hsuq: s/u ∈ ℚ) by (apply ratMul_ran; auto).
          assert (Hsu1: s/u <𝐪 Rat 1). {
            rewrite <- (ratMulInv_annih u)...
            apply ratMul_preserve_lt...
          }
          assert (Hlt: (s/u) ⋅ t <𝐪 t). {
            rewrite <- (ratMul_ident' t) at 2...
            apply ratMul_preserve_lt...
          }
          assert (Hsutq: (s/u) ⋅ t ∈ ℚ) by (apply ratMul_ran; auto).
          assert (Hnnsum: ratNonNeg ((s/u) ⋅ t + v)). {
            left. apply ratAdd_pos_sum...
            apply ratMul_pos_prod... apply ratMul_pos_prod...
          }
          replace (s⋅t + u⋅v) with (u⋅((s/u)⋅t + v)).
          apply realNonNegMulI1... apply realAddI2...
          eapply realE2; revgoals; [eauto|nauto..]. left...
          rewrite ratMul_distr, (ratMul_comm s), <- ratMul_assoc,
            <- (ratMul_assoc u), ratMulInv_annih, ratMul_ident';
            try apply ratMul_ran...
        } {
          assert (Hs': s ∈ ℚ'). {
            apply nzRatI0... apply rat_neq_0...
          }
          assert (Hrsq: s⁻¹ ∈ ℚ). {
            apply nzRatE1. apply ratMulInv_ran...
          }
          assert (Hprs: ratPos s⁻¹) by (apply ratPos_mulInv; auto).
          assert (Husq: u/s ∈ ℚ) by (apply ratMul_ran; auto).
          assert (Hus1: u/s <𝐪 Rat 1). {
            rewrite <- (ratMulInv_annih s)...
            apply ratMul_preserve_lt...
          }
          assert (Hlt: (u/s) ⋅ v <𝐪 v). {
            rewrite <- (ratMul_ident' v) at 2...
            apply ratMul_preserve_lt...
          }
          assert (Hustq: (u/s) ⋅ v ∈ ℚ) by (apply ratMul_ran; auto).
          assert (Hnnsum: ratNonNeg (t + (u/s) ⋅ v)). {
            left. apply ratAdd_pos_sum...
            apply ratMul_pos_prod... apply ratMul_pos_prod...
          }
          replace (s⋅t + u⋅v) with (s⋅(t + (u/s)⋅v)).
          apply realNonNegMulI1... apply realAddI2...
          eapply realE2; revgoals; [eauto|nauto..]. left...
          rewrite ratMul_distr, (ratMul_comm u), <- ratMul_assoc,
            <- (ratMul_assoc s), ratMulInv_annih, ratMul_ident';
            try apply ratMul_ran...
        }
Qed.

Close Scope Rat_scope.
Open Scope Real_scope.

Lemma realNonNegMul_distr' : ∀ x y z ∈ ℝ,
  realNonNeg x → realNonNeg y → realNonNeg z → realNonNeg (y - z) →
  x ⋅₊ (y - z) = x ⋅₊ y - x ⋅₊ z.
Proof with neauto.
  intros x Hx y Hy z Hz Hnnx Hnny Hnnz Hd.
  assert (Hnzr: -z ∈ ℝ) by (apply realAddInv_ran; auto).
  assert (Hxzr: x ⋅₊ z ∈ ℝ) by (apply realNonNegMul_ran; auto).
  assert (Hxyr: x ⋅₊ y ∈ ℝ) by (apply realNonNegMul_ran; auto).
  assert (Hnxzr: -(x ⋅₊ z) ∈ ℝ) by (apply realAddInv_ran; auto).
  assert (Hdr: y - z ∈ ℝ) by (apply realAdd_ran; auto).
  assert (Hxdr: x ⋅₊ (y - z) ∈ ℝ) by (apply realNonNegMul_ran; auto).
  assert (Hdistr: x ⋅₊ y - x ⋅₊ z ∈ ℝ) by (apply realAdd_ran; auto).
  apply (realAdd_cancel _ Hxdr _ Hdistr _ Hxzr).
  rewrite <- realNonNegMul_distr,
    realAdd_assoc, (realAdd_comm (-z)),
    realAddInv_annih, realAdd_ident,
    realAdd_assoc, (realAdd_comm (-(x ⋅₊ z))),
    realAddInv_annih, realAdd_ident...
Qed.

Close Scope Real_scope.
Open Scope Rat_scope.

Lemma realNonNegMul_ident : ∀x ∈ ℝ,
  realNonNeg x → (x ⋅₊ Real 1)%r  = x.
Proof with neauto.
  intros x Hx Hnnx.
  apply ExtAx. intros p. split; intros Hp.
  - apply realNonNegMulE in Hp as []...
    + destruct Hnnx as [Hpx|]; [|subst; auto].
      apply SepE in H as [Hpq Hlt].
      eapply realE2; revgoals... apply realPos_rat0...
    + destruct H as [q [Hqq [r [Hrq [[Hq Hr] [[Hnnq Hnnr] Heq]]]]]].
      destruct Hnnq as [Hpq|Hq0]; revgoals; subst.
      rewrite ratMul_0_l... eapply realE2; revgoals...
      rewrite <- (ratMul_ident q) at 2... apply ratMul_preserve_lt'...
      apply SepE2 in Hr... apply ratMul_ran...
  - destruct (classic (ratNeg p)). apply realNonNegMulI0...
    assert (Hpq: p ∈ ℚ) by (eapply real_sub_rat; eauto).
    apply ratNonNeg_not_neg in H...
    apply realE3 in Hp as [q [Hqq [Hq Hlt]]]...
    assert (Hpoq: ratPos q). {
      destruct H. eapply ratLt_tranr... subst...
    }
    assert (Hprq: ratPos q⁻¹)
      by (apply ratPos_mulInv; auto).
    assert (Hqq': q ∈ ℚ'). {
      apply nzRatI0... apply rat_neq_0...
    }
    assert (Hrqq: q⁻¹ ∈ ℚ). {
      apply nzRatE1. apply ratMulInv_ran...
    }
    replace p with (q ⋅ (p/q)).
    apply realNonNegMulI1... apply SepI.
    apply ratMul_ran... rewrite <- (ratMulInv_annih q)...
    apply ratMul_preserve_lt... left...
    apply ratMul_nonNeg_prod... left...
    rewrite (ratMul_comm p), <- ratMul_assoc,
      ratMulInv_annih, ratMul_ident'...
Qed.

Lemma realNonNegMul_ident' : ∀x ∈ ℝ,
  realNonNeg x → (Real 1 ⋅₊ x)%r  = x.
Proof with nauto.
  intros x Hx Hnnx.
  rewrite realNonNegMul_comm, realNonNegMul_ident...
  left. apply realPos_sn.
Qed.

Close Scope Rat_scope.
Open Scope Real_scope.

(* 正实数乘法逆元 *)
Definition RealPosMulInv : set → set := λ x,
  {r ∊ ℚ | λ r, ∃s ∈ ℚ, s ∉ x ∧ (r ⋅ s)%q <𝐪 Rat 1}.
Notation "x ⁻¹⁺" := (RealPosMulInv x) (at level 9) : Real_scope.

Lemma realPosMulInv_sub_rat : ∀x ∈ ℝ, x⁻¹⁺ ∈ 𝒫 ℚ.
Proof with auto.
  intros x Hx. apply PowerAx. intros q Hq.
  unfold RealPosMulInv in Hq. apply SepE1 in Hq...
Qed.

Close Scope Real_scope.
Open Scope Rat_scope.

Lemma ratLt_mulInv': ∀ q r ∈ ℚ, ratPos r → q <𝐪 r⁻¹ ↔ q ⋅ r <𝐪 Rat 1.
Proof with auto.
  intros q Hq r Hr Hpr.
  assert (Hr': r ∈ ℚ'). { apply nzRatI0... apply rat_neq_0... }
  assert (Hrr: r⁻¹ ∈ ℚ). { apply nzRatE1. apply ratMulInv_ran... }
  split; intros.
  - rewrite <- (ratMulInv_annih r), ratMul_comm...
    apply ratMul_preserve_lt'...
  - rewrite <- (ratMulInv_annih r), ratMul_comm in H...
    apply ratMul_preserve_lt' in H...
Qed.

Lemma realPosMulInv_ran : ∀x ∈ ℝ, realPos x → (x⁻¹⁺)%r ∈ ℝ.
Proof with neauto.
  intros x Hx Hpx. apply SepI.
  apply realPosMulInv_sub_rat...
  apply realPos_rat0 in Hpx... repeat split...
  - destruct (classic (x ≤ Real 1)%r).
    + apply realLeq in H as Hsub... 
      pose proof (realE3 _ Hx _ Hpx) as [q [Hqq [Hqx H0q]]].
      pose proof (realE3 _ Hx _ Hqx) as [r [Hrq [Hrx Hqr]]].
      apply Hsub in Hqx as Hq1. apply SepE in Hq1 as [_ Hq1].
      apply Hsub in Hrx as Hr1. apply SepE in Hr1 as [_ Hr1].
      assert (Hpr: ratPos r) by (eapply ratLt_tranr; eauto).
      apply ratLt_mulInv in Hr1... rewrite ratMulInv_1 in Hr1.
      assert (Hr': r ∈ ℚ'). { apply nzRatI0... apply rat_neq_0... }
      assert (Hrr: r⁻¹ ∈ ℚ). { apply nzRatE1. apply ratMulInv_ran... }
      assert (H1x: Rat 1 ∉ x) by (apply realLt_realn'; auto).
      assert (Hrrx: r⁻¹ ∉ x) by (apply (realE2_2 _ Hx (Rat 1)); nauto).
      apply EmptyNI. exists q. apply SepI... exists (r⁻¹).
      repeat split... rewrite <- (ratMulInv_annih r)...
      apply ratMul_preserve_lt... apply ratPos_mulInv...
    + apply not_or_and in H as [].
      apply realLt_connected in H0 as []...
      apply realLt_realn in H0 as H1x...
      pose proof (realE1 _ Hx) as [q [Hqq Hqx]].
      pose proof (rat_archimedean _ Hqq) as [r [Hrq Hqr]].
      assert (H1q: Rat 1 <𝐪 q) by (eapply realE2_1; neauto).
      assert (H1r: Rat 1 <𝐪 r) by (eapply ratLt_tranr; eauto).
      assert (Hpr: ratPos r). {
        eapply ratLt_tranr; revgoals. apply H1r. apply ratPos_sn.
      }
      assert (Hr': r ∈ ℚ'). { apply nzRatI0... apply rat_neq_0... }
      assert (Hrr: r⁻¹ ∈ ℚ). { apply nzRatE1. apply ratMulInv_ran... }
      apply ratLt_mulInv in H1r as Hr1... rewrite ratMulInv_1 in Hr1.
      apply EmptyNI. exists (r⁻¹). apply SepI... exists q.
      repeat split... rewrite <- (ratMulInv_annih r), ratMul_comm...
      apply ratMul_preserve_lt... apply ratPos_mulInv...
  - pose proof (realE3 _ Hx _ Hpx) as [q [Hqq [Hqx H0q]]].
    assert (Hq': q ∈ ℚ'). { apply nzRatI0... apply rat_neq_0... }
    assert (Hrq: q⁻¹ ∈ ℚ). { apply nzRatE1. apply ratMulInv_ran... }
    apply ExtNI. exists (q⁻¹). split... intros Hrqrx.
    apply SepE in Hrqrx as [_ [s [Hsq [Hsx Hlt]]]].
    rewrite <- (ratMulInv_annih q), ratMul_comm in Hlt...
    apply ratMul_preserve_lt in Hlt; auto; [|apply ratPos_mulInv]...
    apply Hsx. eapply realE2; revgoals...
  - intros p Hpq q Hqq Hp Hlt.
    apply SepE in Hp as [_ [r [Hrq [Hrx Hr1]]]].
    assert (Hpr: ratPos r) by (eapply realE2_1; neauto).
    apply SepI... exists r. repeat split...
    apply ratLt_mulInv' in Hr1...
    apply ratLt_mulInv'... eapply ratLt_tranr...
  - intros p Hp. apply SepE in Hp as [Hpq [r [Hrq [Hrx Hpr1]]]].
    assert (Hpr: ratPos r) by (eapply realE2_1; neauto).
    assert (Hr': r ∈ ℚ'). { apply nzRatI0... apply rat_neq_0... }
    assert (Hrr: r⁻¹ ∈ ℚ). { apply nzRatE1. apply ratMulInv_ran... }
    destruct (classic (ratNonPos p)) as [Hnpp|Hpp].
    + apply ratPos_mulInv in Hpr as Hprr.
      apply ratDense in Hprr as [q [Hqq [Hq1 Hq2]]]...
      exists q. split. apply SepI... exists r. repeat split...
      apply ratLt_mulInv'... destruct Hnpp.
      eapply ratLt_tranr... subst...
    + apply ratPos_not_nonPos in Hpp...
      destruct (classic (p <𝐪 Rat 1)) as [Hp1|H1p];
      destruct (classic (r <𝐪 Rat 1)) as [Hr1|H1r].
      * exists (Rat 1). split... apply SepI...
        exists r. repeat split... rewrite ratMul_ident'...
      * apply ratLt_mulInv' in Hpr1...
        apply ratDense in Hpr1 as [q [Hqq [Hq1 Hq2]]]...
        exists q. split... apply SepI... exists r. repeat split...
        destruct (classic (r = Rat 1)).
        subst. rewrite ratMulInv_1 in Hq2. rewrite ratMul_ident...
        apply ratLt_connected in H as []...
        exfalso... apply ratLt_mulInv'...
      * apply ratLt_mulInv' in Hpr1...
        apply ratDense in Hpr1 as [q [Hqq [Hq1 Hq2]]]...
        exists q. split... apply SepI... exists r. repeat split...
        apply ratLt_mulInv'...
      * exfalso. apply H1p. destruct (classic (r = Rat 1)).
        subst. rewrite ratMul_ident in Hpr1...
        apply ratLt_connected in H as []... exfalso...
        apply ratLt_mulInv in H... rewrite ratMulInv_1 in H.
        apply ratLt_mulInv' in Hpr1... eapply ratLt_tranr...
Qed.

Lemma ex5_19' : ∀x ∈ ℝ, ∀p ∈ ℚ, realPos x → Rat 1 <𝐪 p →
  ∃q ∈ ℚ, ratPos q ∧ q ∈ x ∧ p ⋅ q ∉ x.
Proof with nauto.
  intros x Hx p Hp Hpx H1p. apply realPos_rat0 in Hpx...
  pose proof (realE3 _ Hx _ Hpx) as [r [Hr [Hrx Hpr]]].
  set (p - Rat 1) as p'.
  set (p' ⋅ r / Rat 3) as s.
  assert (Hp': p' ∈ ℚ) by (apply ratAdd_ran; nauto).
  assert (Hs: s ∈ ℚ). {
    apply ratMul_ran. apply ratMul_ran... nauto.
  }
  assert (Hpp': ratPos p'). {
    unfold ratPos. rewrite <- (ratAddInv_annih (Rat 1))...
    apply ratAdd_preserve_lt...
  }
  assert (Hps: ratPos s). {
    apply ratMul_pos_prod. apply ratMul_ran... nauto.
    apply ratMul_pos_prod... nauto.
  }
  pose proof (ex5_19 _ Hx _ Hs Hps) as [t [Ht [Htx Hleft]]].
  destruct (classic (r / Rat 3 <𝐪 t)).
  - assert (Hnt: -t ∈ ℚ) by (apply ratAddInv_ran; auto).
    assert (Hst: s + t ∈ ℚ) by (apply ratAdd_ran; auto).
    assert (Hpt: p ⋅ t ∈ ℚ) by (apply ratMul_ran; auto).
    cut (s + t <𝐪 p ⋅ t). intros Hlt.
    * exists t. repeat split; [auto| |auto|].
      eapply ratLt_tranr; revgoals; [eauto|apply ratMul_pos_prod]...
      eapply realE2_2; revgoals; [apply Hlt|..]; assumption.
    * eapply ratAdd_preserve_lt; swap 1 3; [apply Hnt|auto..|].
      rewrite ratAdd_assoc, ratAddInv_annih, ratAdd_ident; [|auto..].
      rewrite <- (ratMul_ident' t) at 2; [|auto..].
      rewrite <- ratMul_addInv_l, <- ratMul_distr'; [|nauto..].
      unfold s. rewrite ratMul_assoc; [|nauto..]. subst p'.
      apply ratMul_preserve_lt'; [apply ratMul_ran|..]...
  - exists (r / Rat 2). repeat split.
    + apply ratMul_ran... + apply ratMul_pos_prod...
    + cut (r / Rat 2 <𝐪 r). intros Hlt.
      * eapply realE2; swap 1 5; [apply Hlt| |auto..].
        apply ratMul_ran... 
      * rewrite ratMul_comm... rewrite <- (ratMul_ident' r) at 2.
        apply ratMul_preserve_lt... apply ratLt_r2_1. auto.
    + cut (s + t <𝐪 p ⋅ (r / Rat 2)). intros Hlt.
      * eapply realE2_2; swap 1 5; [apply Hlt|..|auto|auto].
        apply ratAdd_ran... apply ratMul_ran; [auto|apply ratMul_ran]...
      * assert (H1: r / Rat 3 ∈ ℚ) by (apply ratMul_ran; nauto).
        assert (H2: -(r / Rat 3) ∈ ℚ) by (apply ratAddInv_ran; nauto).
        assert (H3: p ⋅ r ∈ ℚ) by (apply ratMul_ran; auto).
        assert (H4: p ⋅ r / Rat 3 ∈ ℚ) by (apply ratMul_ran; nauto).
        assert (H5: - Rat 1 + p ∈ ℚ) by (apply ratAdd_ran; nauto).
        rewrite ratAdd_comm; [|auto..]. unfold s, p'.
        rewrite (ratAdd_comm p), ratMul_assoc, ratMul_distr',
          <- ratMul_assoc, <- ratMul_assoc, <- ratMul_assoc,
          ratMul_addInv_l, ratMul_ident', ratMul_addInv_l,
          <- ratAdd_assoc; [|nauto..].
        replace (p⋅r/Rat 2) with (p⋅r / Rat 6 + p⋅r / Rat 3). {
          apply ratAdd_preserve_lt. apply ratAdd_ran...
          repeat apply ratMul_ran... repeat apply ratMul_ran...
          cut (ratPos (p⋅r / Rat 6)). intros Hp6.
          - destruct (classic (t = r/Rat 3)).
            + subst. rewrite ratAddInv_annih; assumption.
            + eapply ratLt_tranr; revgoals. apply Hp6.
              apply ratLt_connected in H0 as []; [|exfalso|auto..]...
              rewrite <- (ratAddInv_annih (r/Rat 3)).
              apply ratAdd_preserve_lt; assumption. apply H1.
          - apply ratMul_pos_prod; [auto|nauto|..|nauto].
            apply ratMul_pos_prod... eapply ratLt_tranr.
            apply ratPos_sn. apply H1p. 
        } {
          rewrite <- ratMul_distr...
          cut ((Rat 6)⁻¹ + (Rat 3)⁻¹ = (Rat 2)⁻¹). congruence.
          apply ratAdd_r6_r3_r2.
        }
Qed.

Theorem realPosMulInv_annih : ∀x ∈ ℝ,
  realPos x → (x ⋅₊ x⁻¹⁺)%r = Real 1.
Proof with neauto.
  intros x Hx Hposx.
  assert (Hx': (x⁻¹⁺)%r ∈ ℝ) by (apply realPosMulInv_ran; auto).
  apply ExtAx. intros p. split; intros Hp.
  - apply realNonNegMulE in Hp as [Hp0|Hp]...
    + apply SepE in Hp0 as [Hpq Hp0]. apply SepI...
      eapply ratLt_tranr... apply ratPos_sn.
    + destruct Hp as [q [Hqq [r [Hrq [[Hq Hr] [[Hnnq Hnnr] Heq]]]]]].
      subst p. apply SepI. apply ratMul_ran...
      destruct Hnnq; destruct Hnnr; revgoals; subst.
      * rewrite ratMul_0_l... apply ratPos_sn.
      * rewrite ratMul_0_l... apply ratPos_sn.
      * rewrite ratMul_0_r... apply ratPos_sn.
      * apply SepE in Hr as [_ [s [Hsq [Hsx Hlt]]]].
        assert (Hqs: q <𝐪 s) by (eapply realE2_1; revgoals; eauto).
        assert (Hps: ratPos s) by (eapply ratLt_tranr; revgoals; eauto).
        rewrite ratMul_comm in Hlt... apply ratLt_mulInv' in Hlt...
        apply ratLt_mulInv'... eapply ratLt_tranr...
  - apply SepE in Hp as [Hpq Hp1].
    destruct (classic (p = Rat 0)). {
      apply realPos_rat0 in Hposx...
      subst p. rewrite <- (ratMul_0_l (Rat 0))...
      apply realNonNegMulI1; auto; [|right..]...
      pose proof (realE1 _ Hx) as [q [Hqq Hqx]].
      apply SepI... exists q. repeat split... rewrite ratMul_0_l...
    }
    apply ratLt_connected in H as [Hnp|Hpp]... {
      eapply realNonNegMulI0...
    }
    assert (Hpq': p ∈ ℚ'). { apply nzRatI0... apply rat_neq_0... }
    assert (Hrpq: p⁻¹ ∈ ℚ). { apply nzRatE1. apply ratMulInv_ran... }
    assert (Hprp: ratPos p⁻¹) by (apply ratPos_mulInv; auto).
    apply ratLt_mulInv in Hp1... rewrite ratMulInv_1 in Hp1.
    pose proof (ex5_19' _ Hx _ Hrpq Hposx Hp1) as [q [Hqq [Hposq [Hqx Hs]]]].
    pose proof (realE3 _ Hx _ Hqx) as [r [Hrq [Hrx Hqr]]].
    assert (Hposr: ratPos r) by (eapply ratLt_tranr; eauto).
    assert (Hrq': r ∈ ℚ'). { apply nzRatI0... apply rat_neq_0... }
    assert (Hrrq: r⁻¹ ∈ ℚ). { apply nzRatE1. apply ratMulInv_ran... }
    assert (Hsq: q / p ∈ ℚ) by (apply ratMul_ran; auto).
    assert (Htq: p / r ∈ ℚ) by (apply ratMul_ran; auto).
    assert (Hpt: ratPos (p / r)). {
      apply ratMul_pos_prod... apply ratPos_mulInv...
    }
    rewrite <- (ratMul_ident' p), <- (ratMulInv_annih r),
      ratMul_assoc, (ratMul_comm (r⁻¹))...
    apply realNonNegMulI1; auto; revgoals; [left|left|]...
    apply SepI. apply ratMul_ran... exists (q / p). repeat split...
    rewrite ratMul_comm... rewrite (ratMul_comm (p / r))...
    apply ratLt_mulInv'... rewrite ratMulInv_quot...
    apply ratMul_preserve_lt...
Qed.

Lemma realPos_posMulInv : ∀x ∈ ℝ, realPos x → realPos (x⁻¹⁺)%r.
Proof with neauto.
  intros x Hx Hpx. apply realPos_rat0 in Hpx as H0x...
  apply binRelI... apply realPosMulInv_ran...
  pose proof (realE1 _ Hx) as [q [Hqq Hqx]]. 
  assert (Hposq: ratPos q) by (eapply realE2_1; neauto). split.
  - intros p Hp. apply SepE in Hp as [Hpq Hnp].
    apply SepI... exists q. repeat split... eapply ratLt_tranr.
    rewrite ratMul_comm... apply ratMul_neg_prod... apply ratPos_sn.
  - pose proof (rat_archimedean _ Hqq) as [r [Hrq Hqr]].
    assert (Hposr: ratPos r) by (eapply ratLt_tranr; eauto).
    assert (Hr': r ∈ ℚ'). { apply nzRatI0... apply rat_neq_0... }
    assert (Hrr: r⁻¹ ∈ ℚ). { apply nzRatE1. apply ratMulInv_ran... }
    assert (Hposrr: ratPos r⁻¹) by (apply ratPos_mulInv; auto).
    cut (r⁻¹ ∈ (x⁻¹⁺)%r). intros Hrqrx.
    intros H. rewrite ExtAx in H. apply H in Hrqrx.
    apply SepE in Hrqrx as [_ Hnrr].
    eapply ratLt_irrefl. eapply ratLt_tranr...
    apply SepI... exists q. repeat split... rewrite ratMul_comm...
    apply ratLt_mulInv'... rewrite ratMulInv_double...
Qed.

Close Scope Rat_scope.
Open Scope Real_scope.

Lemma realPosMulInv_double : ∀x ∈ ℝ, realPos x → x⁻¹⁺⁻¹⁺ = x.
Proof with auto.
  intros x Hx Hpx.
  assert (Hr: x⁻¹⁺ ∈ ℝ) by (apply realPosMulInv_ran; auto).
  assert (Hpr: realPos x⁻¹⁺) by (apply realPos_posMulInv; auto).
  assert (Hrr: x⁻¹⁺⁻¹⁺ ∈ ℝ) by (apply realPosMulInv_ran; auto).
  assert (Hprr: realPos x⁻¹⁺⁻¹⁺) by (apply realPos_posMulInv; auto).
  rewrite <- (realNonNegMul_ident (x⁻¹⁺⁻¹⁺)), <- (realPosMulInv_annih x),
    realNonNegMul_comm, realNonNegMul_assoc, realPosMulInv_annih,
    realNonNegMul_ident; try left...
  apply realNonNegMul_ran; try left...
  apply realNonNegMul_pos_prod...
Qed.
